Step of Proof: fincr_wf2 12,41
Inference at * 1 4 1 1 
Iof proof for Lemma fincr wf2:



1. i : 
2. f : {f | i:{z:| z < i}   if (i = 0) then  else {f(i - 1)...} fi }
3. j : {k:| k < i} 
  f(j)   
latex
 by ((D (-1)) 
CollapseTHEN (CompNatInd (-2))) 
latex

C1: 

C1: 3. j : 
C1: 4. j1:. (j1 < j)  (j1 < i)  (f(j1)  )
C1:   (j < i)  (f(j)  )
C.

Definitions, , False, A, A  B, i  j , P  Q, x:A. B(x), t  T
Lemmasle wf, nat wf, ge wf, nat properties

origin